(set-logic QF_UF)
(declare-fun uf3 (Bool Bool Bool) Bool)
(declare-fun uf4 (Bool Bool Bool Bool) Bool)
(declare-fun uf5 (Bool Bool Bool Bool Bool) Bool)
(declare-fun uf6 (Bool Bool Bool Bool Bool Bool) Bool)
(declare-fun v0 () Bool)
(declare-fun v4 () Bool)
(push 1)
(assert (uf5 v0 false v4 true false))
(check-sat)
(check-sat)
(assert false)
(check-sat)
(pop 1)
(check-sat)
(declare-fun v18 () Bool)
(declare-fun v20 () Bool)
(assert (uf4 v4 false true true))
(push 1)
(assert (uf3 v18 (=> v0 (uf4 v4 false true true)) false))
(check-sat)
(assert (uf5 v20 true false true true))
(assert v4)
(check-sat)
(check-sat)
(assert false)
(check-sat)
(pop 1)
(check-sat)
(assert (uf6 true v18 (=> v18 v20) true true true))
(check-sat)
